package edu.uic.cs.cs582.process.impl;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.TreeSet;

import org.apache.commons.lang.ArrayUtils;

import edu.uic.cs.cs582.data.Component;
import edu.uic.cs.cs582.data.Polarity;
import edu.uic.cs.cs582.misc.Assert;

/**
 * Please co-reference {@link SatIndexParser}
 *
 */
public abstract class AbstractVariablesOperations
{
	protected Component component;

	protected AbstractVariablesOperations(Component component)
	{
		this.component = component;
	}

	/**
	 * Can ONLY be used before variable!!!
	 * 
	 * @param exp
	 * @return
	 */
	protected int not(int exp)
	{
		return 0 - exp;
	}

	protected int positiveSymbol(int synsetIndex)
	{
		return (synsetIndex << SatIndexParser.SAT_VARIABLE_SUFFIX_LENGTH)
				+ SatIndexParser.SAT_VARIABLE_SUFFIX_POSITIVE;
	}

	protected int negativeSymbol(int synsetIndex)
	{
		return (synsetIndex << SatIndexParser.SAT_VARIABLE_SUFFIX_LENGTH)
				+ SatIndexParser.SAT_VARIABLE_SUFFIX_NEGATIVE;
	}

	protected int polarSymbol(Polarity polarity, int synsetIndex)
	{
		if (polarity == Polarity.POSITIVE)
		{
			return positiveSymbol(synsetIndex);
		}
		else if (polarity == Polarity.NEGATIVE)
		{
			return negativeSymbol(synsetIndex);
		}
		else
		{
			Assert.isTrue(false,
					"Should not use NEUTRAL symbol, use (NOT POSITIVE AND NOT NEGATIVE) instead! ");
			return -1;
		}
	}

	protected int frequencyDigitSymbol(long variableIndex,
			int wordIndexInComponent)
	{
		int wordIndexOffset = component.getWordsNumberBinaryLength();

		long result = (((variableIndex << wordIndexOffset) + wordIndexInComponent) << SatIndexParser.SAT_VARIABLE_SUFFIX_LENGTH)
				+ SatIndexParser.SAT_VARIABLE_SUFFIX_FREQUENCY_DIGIT;
		if (result > Integer.MAX_VALUE)
		{
			Assert.isTrue(false, "Frequency digit symbol generated[" + result
					+ "(" + Long.toBinaryString(result)
					+ ")] exceed max integer value - " + Integer.MAX_VALUE);
		}

		return (int) result;
	}

	////////////////////////////////////////////////////////////////////////////
	protected List<int[]> convertDnfToCnf(List<int[]> dnfs)
	{
		TreeSet<int[]> oneDnfList = new TreeSet<int[]>(new IntArrayComparator());
		for (int dnf : dnfs.get(0))
		{
			oneDnfList.add(new int[] { dnf });
		}

		if (dnfs.size() == 1)
		{
			return new ArrayList<int[]>(oneDnfList);
		}

		for (int index = 1; index < dnfs.size(); index++)
		{
			if (oneDnfList.isEmpty())
			{
				return Collections.emptyList();
			}

			int[] anotherDnf = dnfs.get(index);
			oneDnfList = convertTwoDnfToOneCnf(oneDnfList, anotherDnf);
		}

		// use absorption rule to remove some expressions
		// a or (a and b) = a; 
		// Since we are deleting something, we use LinkedList for performance improvement
		List<int[]> resultCnfClauses = getFinalCnfClausesAfterAdoptAbsorptionRule(oneDnfList);

		return resultCnfClauses;
	}

	List<int[]> getFinalCnfClausesAfterAdoptAbsorptionRule(
			TreeSet<int[]> cnfClauses)
	{
		LinkedList<int[]> resultCnfClauses = new LinkedList<int[]>(cnfClauses);

		HashSet<Integer> indicesListToRemove = getIndicesToRemoveByAbsorptionRule(resultCnfClauses);
		Integer[] indicesArrayToRemove = indicesListToRemove
				.toArray(new Integer[indicesListToRemove.size()]);

		Arrays.sort(indicesArrayToRemove);
		for (int index = indicesArrayToRemove.length - 1; index >= 0; index--)
		{
			// remove elements from rear to front
			resultCnfClauses.remove(indicesArrayToRemove[index].intValue());
		}

		return resultCnfClauses;

		//		try to find a more efficient way to do this removing, instead of 'new' twice 
		//		TreeSet<int[]> result = new TreeSet<int[]>(new IntArrayComparator());
		//		result.addAll(resultCnfClauses);
		//
		//		return result;
	}

	private HashSet<Integer> getIndicesToRemoveByAbsorptionRule(
			LinkedList<int[]> resultDnfClauses)
	{
		HashSet<Integer> indicesToRemove = new HashSet<Integer>();
		int totlaLength = resultDnfClauses.size();
		int indexOfNextLongerOne = 1;
		for (int i = 0; i < totlaLength; i++)
		{
			// already known to be removed
			if (indicesToRemove.contains(i))
			{
				continue;
			}

			int[] one = resultDnfClauses.get(i);
			indexOfNextLongerOne = (indexOfNextLongerOne > i + 1) ? indexOfNextLongerOne
					: (i + 1);
			for (int j = indexOfNextLongerOne; j < totlaLength; j++)
			{
				// already known to be removed
				if (indicesToRemove.contains(j))
				{
					if (indexOfNextLongerOne == j)
					{
						indexOfNextLongerOne = j + 1;
					}
					continue;
				}

				int[] another = resultDnfClauses.get(j);
				// Already sorted by length
				if (one.length == another.length)
				{
					indexOfNextLongerOne = j + 1;
					continue;
				}

				// Assert.isTrue(one.length < another.length);
				// if larger one contains the smaller one, then remove the larger one 
				if (containsAll(another, one))
				{
					indicesToRemove.add(j);
				}
			}

			if (indexOfNextLongerOne >= totlaLength)
			{
				break;
			}
		}
		return indicesToRemove;
	}

	private boolean containsAll(int[] larger, int[] smaller)
	{
		for (int smallOne : smaller)
		{
			if (!ArrayUtils.contains(larger, smallOne))
			{
				return false;
			}
		}

		return true;
	}

	private TreeSet<int[]> convertTwoDnfToOneCnf(TreeSet<int[]> oneDnfs,
			int[] anotherDnf)
	{
		TreeSet<int[]> result = new TreeSet<int[]>(new IntArrayComparator());
		int[] newArray = null;

		for (int[] eachInOne : oneDnfs)
		{
			for (int eachInAnother : anotherDnf)
			{
				if (Arrays.binarySearch(eachInOne, eachInAnother) >= 0)
				{
					result.add(eachInOne);
					continue;
				}

				// a OR NOT a = 1; 1 AND any = any 
				if (Arrays.binarySearch(eachInOne, not(eachInAnother)) >= 0)
				{
					continue;
				}

				newArray = Arrays.copyOf(eachInOne, eachInOne.length + 1);
				newArray[newArray.length - 1] = eachInAnother;
				Arrays.sort(newArray);

				result.add(newArray);
			}
		}

		return result;

	}

}